active1(f3(a, b, X)) -> mark1(f3(X, X, X))
active1(c) -> mark1(a)
active1(c) -> mark1(b)
active1(f3(X1, X2, X3)) -> f3(active1(X1), X2, X3)
active1(f3(X1, X2, X3)) -> f3(X1, X2, active1(X3))
f3(mark1(X1), X2, X3) -> mark1(f3(X1, X2, X3))
f3(X1, X2, mark1(X3)) -> mark1(f3(X1, X2, X3))
proper1(f3(X1, X2, X3)) -> f3(proper1(X1), proper1(X2), proper1(X3))
proper1(a) -> ok1(a)
proper1(b) -> ok1(b)
proper1(c) -> ok1(c)
f3(ok1(X1), ok1(X2), ok1(X3)) -> ok1(f3(X1, X2, X3))
top1(mark1(X)) -> top1(proper1(X))
top1(ok1(X)) -> top1(active1(X))
↳ QTRS
↳ DependencyPairsProof
active1(f3(a, b, X)) -> mark1(f3(X, X, X))
active1(c) -> mark1(a)
active1(c) -> mark1(b)
active1(f3(X1, X2, X3)) -> f3(active1(X1), X2, X3)
active1(f3(X1, X2, X3)) -> f3(X1, X2, active1(X3))
f3(mark1(X1), X2, X3) -> mark1(f3(X1, X2, X3))
f3(X1, X2, mark1(X3)) -> mark1(f3(X1, X2, X3))
proper1(f3(X1, X2, X3)) -> f3(proper1(X1), proper1(X2), proper1(X3))
proper1(a) -> ok1(a)
proper1(b) -> ok1(b)
proper1(c) -> ok1(c)
f3(ok1(X1), ok1(X2), ok1(X3)) -> ok1(f3(X1, X2, X3))
top1(mark1(X)) -> top1(proper1(X))
top1(ok1(X)) -> top1(active1(X))
ACTIVE1(f3(X1, X2, X3)) -> ACTIVE1(X1)
TOP1(mark1(X)) -> PROPER1(X)
ACTIVE1(f3(X1, X2, X3)) -> ACTIVE1(X3)
PROPER1(f3(X1, X2, X3)) -> PROPER1(X1)
ACTIVE1(f3(X1, X2, X3)) -> F3(active1(X1), X2, X3)
PROPER1(f3(X1, X2, X3)) -> PROPER1(X3)
ACTIVE1(f3(a, b, X)) -> F3(X, X, X)
F3(mark1(X1), X2, X3) -> F3(X1, X2, X3)
TOP1(ok1(X)) -> ACTIVE1(X)
ACTIVE1(f3(X1, X2, X3)) -> F3(X1, X2, active1(X3))
TOP1(ok1(X)) -> TOP1(active1(X))
TOP1(mark1(X)) -> TOP1(proper1(X))
PROPER1(f3(X1, X2, X3)) -> PROPER1(X2)
PROPER1(f3(X1, X2, X3)) -> F3(proper1(X1), proper1(X2), proper1(X3))
F3(X1, X2, mark1(X3)) -> F3(X1, X2, X3)
F3(ok1(X1), ok1(X2), ok1(X3)) -> F3(X1, X2, X3)
active1(f3(a, b, X)) -> mark1(f3(X, X, X))
active1(c) -> mark1(a)
active1(c) -> mark1(b)
active1(f3(X1, X2, X3)) -> f3(active1(X1), X2, X3)
active1(f3(X1, X2, X3)) -> f3(X1, X2, active1(X3))
f3(mark1(X1), X2, X3) -> mark1(f3(X1, X2, X3))
f3(X1, X2, mark1(X3)) -> mark1(f3(X1, X2, X3))
proper1(f3(X1, X2, X3)) -> f3(proper1(X1), proper1(X2), proper1(X3))
proper1(a) -> ok1(a)
proper1(b) -> ok1(b)
proper1(c) -> ok1(c)
f3(ok1(X1), ok1(X2), ok1(X3)) -> ok1(f3(X1, X2, X3))
top1(mark1(X)) -> top1(proper1(X))
top1(ok1(X)) -> top1(active1(X))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
ACTIVE1(f3(X1, X2, X3)) -> ACTIVE1(X1)
TOP1(mark1(X)) -> PROPER1(X)
ACTIVE1(f3(X1, X2, X3)) -> ACTIVE1(X3)
PROPER1(f3(X1, X2, X3)) -> PROPER1(X1)
ACTIVE1(f3(X1, X2, X3)) -> F3(active1(X1), X2, X3)
PROPER1(f3(X1, X2, X3)) -> PROPER1(X3)
ACTIVE1(f3(a, b, X)) -> F3(X, X, X)
F3(mark1(X1), X2, X3) -> F3(X1, X2, X3)
TOP1(ok1(X)) -> ACTIVE1(X)
ACTIVE1(f3(X1, X2, X3)) -> F3(X1, X2, active1(X3))
TOP1(ok1(X)) -> TOP1(active1(X))
TOP1(mark1(X)) -> TOP1(proper1(X))
PROPER1(f3(X1, X2, X3)) -> PROPER1(X2)
PROPER1(f3(X1, X2, X3)) -> F3(proper1(X1), proper1(X2), proper1(X3))
F3(X1, X2, mark1(X3)) -> F3(X1, X2, X3)
F3(ok1(X1), ok1(X2), ok1(X3)) -> F3(X1, X2, X3)
active1(f3(a, b, X)) -> mark1(f3(X, X, X))
active1(c) -> mark1(a)
active1(c) -> mark1(b)
active1(f3(X1, X2, X3)) -> f3(active1(X1), X2, X3)
active1(f3(X1, X2, X3)) -> f3(X1, X2, active1(X3))
f3(mark1(X1), X2, X3) -> mark1(f3(X1, X2, X3))
f3(X1, X2, mark1(X3)) -> mark1(f3(X1, X2, X3))
proper1(f3(X1, X2, X3)) -> f3(proper1(X1), proper1(X2), proper1(X3))
proper1(a) -> ok1(a)
proper1(b) -> ok1(b)
proper1(c) -> ok1(c)
f3(ok1(X1), ok1(X2), ok1(X3)) -> ok1(f3(X1, X2, X3))
top1(mark1(X)) -> top1(proper1(X))
top1(ok1(X)) -> top1(active1(X))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
↳ QDP
F3(mark1(X1), X2, X3) -> F3(X1, X2, X3)
F3(ok1(X1), ok1(X2), ok1(X3)) -> F3(X1, X2, X3)
F3(X1, X2, mark1(X3)) -> F3(X1, X2, X3)
active1(f3(a, b, X)) -> mark1(f3(X, X, X))
active1(c) -> mark1(a)
active1(c) -> mark1(b)
active1(f3(X1, X2, X3)) -> f3(active1(X1), X2, X3)
active1(f3(X1, X2, X3)) -> f3(X1, X2, active1(X3))
f3(mark1(X1), X2, X3) -> mark1(f3(X1, X2, X3))
f3(X1, X2, mark1(X3)) -> mark1(f3(X1, X2, X3))
proper1(f3(X1, X2, X3)) -> f3(proper1(X1), proper1(X2), proper1(X3))
proper1(a) -> ok1(a)
proper1(b) -> ok1(b)
proper1(c) -> ok1(c)
f3(ok1(X1), ok1(X2), ok1(X3)) -> ok1(f3(X1, X2, X3))
top1(mark1(X)) -> top1(proper1(X))
top1(ok1(X)) -> top1(active1(X))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
F3(mark1(X1), X2, X3) -> F3(X1, X2, X3)
Used ordering: Polynomial Order [17,21] with Interpretation:
F3(ok1(X1), ok1(X2), ok1(X3)) -> F3(X1, X2, X3)
F3(X1, X2, mark1(X3)) -> F3(X1, X2, X3)
POL( F3(x1, ..., x3) ) = max{0, x1 - 2}
POL( mark1(x1) ) = x1 + 3
POL( ok1(x1) ) = x1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
↳ QDP
F3(X1, X2, mark1(X3)) -> F3(X1, X2, X3)
F3(ok1(X1), ok1(X2), ok1(X3)) -> F3(X1, X2, X3)
active1(f3(a, b, X)) -> mark1(f3(X, X, X))
active1(c) -> mark1(a)
active1(c) -> mark1(b)
active1(f3(X1, X2, X3)) -> f3(active1(X1), X2, X3)
active1(f3(X1, X2, X3)) -> f3(X1, X2, active1(X3))
f3(mark1(X1), X2, X3) -> mark1(f3(X1, X2, X3))
f3(X1, X2, mark1(X3)) -> mark1(f3(X1, X2, X3))
proper1(f3(X1, X2, X3)) -> f3(proper1(X1), proper1(X2), proper1(X3))
proper1(a) -> ok1(a)
proper1(b) -> ok1(b)
proper1(c) -> ok1(c)
f3(ok1(X1), ok1(X2), ok1(X3)) -> ok1(f3(X1, X2, X3))
top1(mark1(X)) -> top1(proper1(X))
top1(ok1(X)) -> top1(active1(X))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
F3(X1, X2, mark1(X3)) -> F3(X1, X2, X3)
Used ordering: Polynomial Order [17,21] with Interpretation:
F3(ok1(X1), ok1(X2), ok1(X3)) -> F3(X1, X2, X3)
POL( F3(x1, ..., x3) ) = max{0, x3 - 2}
POL( mark1(x1) ) = x1 + 3
POL( ok1(x1) ) = x1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
↳ QDP
F3(ok1(X1), ok1(X2), ok1(X3)) -> F3(X1, X2, X3)
active1(f3(a, b, X)) -> mark1(f3(X, X, X))
active1(c) -> mark1(a)
active1(c) -> mark1(b)
active1(f3(X1, X2, X3)) -> f3(active1(X1), X2, X3)
active1(f3(X1, X2, X3)) -> f3(X1, X2, active1(X3))
f3(mark1(X1), X2, X3) -> mark1(f3(X1, X2, X3))
f3(X1, X2, mark1(X3)) -> mark1(f3(X1, X2, X3))
proper1(f3(X1, X2, X3)) -> f3(proper1(X1), proper1(X2), proper1(X3))
proper1(a) -> ok1(a)
proper1(b) -> ok1(b)
proper1(c) -> ok1(c)
f3(ok1(X1), ok1(X2), ok1(X3)) -> ok1(f3(X1, X2, X3))
top1(mark1(X)) -> top1(proper1(X))
top1(ok1(X)) -> top1(active1(X))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
F3(ok1(X1), ok1(X2), ok1(X3)) -> F3(X1, X2, X3)
POL( F3(x1, ..., x3) ) = max{0, x3 - 2}
POL( ok1(x1) ) = x1 + 3
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
↳ QDP
active1(f3(a, b, X)) -> mark1(f3(X, X, X))
active1(c) -> mark1(a)
active1(c) -> mark1(b)
active1(f3(X1, X2, X3)) -> f3(active1(X1), X2, X3)
active1(f3(X1, X2, X3)) -> f3(X1, X2, active1(X3))
f3(mark1(X1), X2, X3) -> mark1(f3(X1, X2, X3))
f3(X1, X2, mark1(X3)) -> mark1(f3(X1, X2, X3))
proper1(f3(X1, X2, X3)) -> f3(proper1(X1), proper1(X2), proper1(X3))
proper1(a) -> ok1(a)
proper1(b) -> ok1(b)
proper1(c) -> ok1(c)
f3(ok1(X1), ok1(X2), ok1(X3)) -> ok1(f3(X1, X2, X3))
top1(mark1(X)) -> top1(proper1(X))
top1(ok1(X)) -> top1(active1(X))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
PROPER1(f3(X1, X2, X3)) -> PROPER1(X1)
PROPER1(f3(X1, X2, X3)) -> PROPER1(X3)
PROPER1(f3(X1, X2, X3)) -> PROPER1(X2)
active1(f3(a, b, X)) -> mark1(f3(X, X, X))
active1(c) -> mark1(a)
active1(c) -> mark1(b)
active1(f3(X1, X2, X3)) -> f3(active1(X1), X2, X3)
active1(f3(X1, X2, X3)) -> f3(X1, X2, active1(X3))
f3(mark1(X1), X2, X3) -> mark1(f3(X1, X2, X3))
f3(X1, X2, mark1(X3)) -> mark1(f3(X1, X2, X3))
proper1(f3(X1, X2, X3)) -> f3(proper1(X1), proper1(X2), proper1(X3))
proper1(a) -> ok1(a)
proper1(b) -> ok1(b)
proper1(c) -> ok1(c)
f3(ok1(X1), ok1(X2), ok1(X3)) -> ok1(f3(X1, X2, X3))
top1(mark1(X)) -> top1(proper1(X))
top1(ok1(X)) -> top1(active1(X))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
PROPER1(f3(X1, X2, X3)) -> PROPER1(X1)
PROPER1(f3(X1, X2, X3)) -> PROPER1(X3)
PROPER1(f3(X1, X2, X3)) -> PROPER1(X2)
POL( PROPER1(x1) ) = max{0, x1 - 2}
POL( f3(x1, ..., x3) ) = x1 + x2 + x3 + 3
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
active1(f3(a, b, X)) -> mark1(f3(X, X, X))
active1(c) -> mark1(a)
active1(c) -> mark1(b)
active1(f3(X1, X2, X3)) -> f3(active1(X1), X2, X3)
active1(f3(X1, X2, X3)) -> f3(X1, X2, active1(X3))
f3(mark1(X1), X2, X3) -> mark1(f3(X1, X2, X3))
f3(X1, X2, mark1(X3)) -> mark1(f3(X1, X2, X3))
proper1(f3(X1, X2, X3)) -> f3(proper1(X1), proper1(X2), proper1(X3))
proper1(a) -> ok1(a)
proper1(b) -> ok1(b)
proper1(c) -> ok1(c)
f3(ok1(X1), ok1(X2), ok1(X3)) -> ok1(f3(X1, X2, X3))
top1(mark1(X)) -> top1(proper1(X))
top1(ok1(X)) -> top1(active1(X))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
ACTIVE1(f3(X1, X2, X3)) -> ACTIVE1(X1)
ACTIVE1(f3(X1, X2, X3)) -> ACTIVE1(X3)
active1(f3(a, b, X)) -> mark1(f3(X, X, X))
active1(c) -> mark1(a)
active1(c) -> mark1(b)
active1(f3(X1, X2, X3)) -> f3(active1(X1), X2, X3)
active1(f3(X1, X2, X3)) -> f3(X1, X2, active1(X3))
f3(mark1(X1), X2, X3) -> mark1(f3(X1, X2, X3))
f3(X1, X2, mark1(X3)) -> mark1(f3(X1, X2, X3))
proper1(f3(X1, X2, X3)) -> f3(proper1(X1), proper1(X2), proper1(X3))
proper1(a) -> ok1(a)
proper1(b) -> ok1(b)
proper1(c) -> ok1(c)
f3(ok1(X1), ok1(X2), ok1(X3)) -> ok1(f3(X1, X2, X3))
top1(mark1(X)) -> top1(proper1(X))
top1(ok1(X)) -> top1(active1(X))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
ACTIVE1(f3(X1, X2, X3)) -> ACTIVE1(X1)
ACTIVE1(f3(X1, X2, X3)) -> ACTIVE1(X3)
POL( ACTIVE1(x1) ) = max{0, x1 - 2}
POL( f3(x1, ..., x3) ) = x1 + x3 + 3
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
active1(f3(a, b, X)) -> mark1(f3(X, X, X))
active1(c) -> mark1(a)
active1(c) -> mark1(b)
active1(f3(X1, X2, X3)) -> f3(active1(X1), X2, X3)
active1(f3(X1, X2, X3)) -> f3(X1, X2, active1(X3))
f3(mark1(X1), X2, X3) -> mark1(f3(X1, X2, X3))
f3(X1, X2, mark1(X3)) -> mark1(f3(X1, X2, X3))
proper1(f3(X1, X2, X3)) -> f3(proper1(X1), proper1(X2), proper1(X3))
proper1(a) -> ok1(a)
proper1(b) -> ok1(b)
proper1(c) -> ok1(c)
f3(ok1(X1), ok1(X2), ok1(X3)) -> ok1(f3(X1, X2, X3))
top1(mark1(X)) -> top1(proper1(X))
top1(ok1(X)) -> top1(active1(X))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
TOP1(ok1(X)) -> TOP1(active1(X))
TOP1(mark1(X)) -> TOP1(proper1(X))
active1(f3(a, b, X)) -> mark1(f3(X, X, X))
active1(c) -> mark1(a)
active1(c) -> mark1(b)
active1(f3(X1, X2, X3)) -> f3(active1(X1), X2, X3)
active1(f3(X1, X2, X3)) -> f3(X1, X2, active1(X3))
f3(mark1(X1), X2, X3) -> mark1(f3(X1, X2, X3))
f3(X1, X2, mark1(X3)) -> mark1(f3(X1, X2, X3))
proper1(f3(X1, X2, X3)) -> f3(proper1(X1), proper1(X2), proper1(X3))
proper1(a) -> ok1(a)
proper1(b) -> ok1(b)
proper1(c) -> ok1(c)
f3(ok1(X1), ok1(X2), ok1(X3)) -> ok1(f3(X1, X2, X3))
top1(mark1(X)) -> top1(proper1(X))
top1(ok1(X)) -> top1(active1(X))